Nuprl Lemma : comb_for_fun_exp_wf
4,23
postcript
pdf
(
T
,
n
,
f
,
z
.
f
^
n
)
T
:Type
(
T
T
)
True
T
T
latex
Definitions
T
,
x
:
A
.
B
(
x
)
,
t
T
,
True
,
Lemmas
nat
wf
,
true
wf
,
squash
wf
,
fun
exp
wf
origin
T,n,f,z. f^n) 
T:Type
(TT)
TrueTT T,n,f,z. f^n) T:Type(TT)TrueTT T
x:A. B(x) T